1. Related Field
The following invention relates to a method and a device configured for carrying out the method for verifying a digital circuit using a model of the circuit and at least one required property of the circuit, and to a digital storage medium with control signals for carrying out the method using a data processing device.
2. Description of the Related Art
As defined herein, a property has an assumption and an assertion. A property is applicable and the circuit possesses this property if, in the presence of the assumption, the assertion occurs or is applicable, both the assumption and the assertion of the property being descriptions of the state of the circuit, in particular while accounting for the time or relative time references. A circuit description of this type does not necessarily provide a complete description of the state of the circuit, but comprises individual state ratings. A state rating of this type can establish, for example, the logic state of a signal line within the circuit, the content of a register or a relationship between a plurality of signals. State descriptions will generally reproduce the state of only a few parts of the circuit.
As a constituent of a property, a state description generally also possesses a time component, so a circuit state is determined not only at a specific instant but also over a specific number of increments in time or over a specific period of time. It can be used to determine, in particular, changes in logic states of specific signals or of a register content together with the timing thereof relevant to other events.
A description of the circuit, which is abstract and generally describes fewer details than the complete circuit design at gate level, is basically produced when defining such properties.
Furthermore, the assumption and assertion of a property are generally in a fixed time relationship with one another so the changes of state defined by the assertion of a property appear with time definition with respect to the changes of state in the corresponding assumption, if the property is applicable. The time ranges spanned by the assumption and the assertion of a property can also overlap, the entire time frame spanned by a property also being designated as the interval of the property.
The assumption and the assertion of a property may be defined by terms from the ITL (interval temporal logic). An identifier for a specific instant which is, for example, t can be introduced into a property as a time reference point. Individual states or changes of state may then be described with respect to this instant, the relative position, in particular, being expressed by means of time increments. For example, an instant which is five time increments behind the reference instant can be identified by t+5.
Moreover, a different time reference system may also be defined within a property, by introducing a further identifier, which is placed in a temporal relationship with the first-mentioned identifier of the instant. This reference can also include a specific interval, so there is a plurality of options for the temporal relationship between the two instants. This is advantageous, for example, in cases where a change in the state of the property is not required at a specific instant, but only the appearance of the change in state within a specific time interval which, in turn, is in a temporal relationship with a further change of state or event.
When verifying a digital circuit using the model circuit and at least one required property, the model circuit is used to check whether the required property is or is not applicable in that an counterexample is sought, which is a concrete description of the state of the circuit and in which the assertion does not apply. To enable this statement to be made, the counterexample fulfils the assumption, so a statement about the property can be made in any case and a contradiction between the counterexample and the assertion appears. This means that the assertion is incompatible with the state description supplied by the counterexample. If a counterexample appears during development of the circuit, it must then be checked whether it is due to the inadequate formulation of the property or whether the circuit design needs to be changed. It is frequently due to inadequate formulation of the property owing, in particular, to the fact that attainability was not analysed during the check for reasons of cost and practicability. This means that the properties have sometimes also been checked on the basis of circuit states which cannot appear in practice or at least should not appear, and these irrelevant states have then led to a counterexample or to the inapplicability of the property. The counterexamples found in such cases are irrelevant as the triggering states do not have to be taken into consideration in practice. A further reason for irrelevant counterexamples may also be that environmental influences from other parts of the circuit, which are being investigated separately, for example, have not been taken into consideration. Therefore, it is basically necessary, when developing a digital circuit by the above-described method, to check the applicability of a property and, on appearance of a counterexample, to investigate the reason for the appearance of the counterexample and possibly to change the property.